textarea {
  resize: none;
  outline: none;
}

#semantics {
  display: flex;
  font-size: 14px;
}

#semantics .opName {
  height: 16px;
  border: 1px solid #c1c1c1;
  border-radius: 3px;
  display: block;
  background-color: white;
  padding: 2px 4px;
  text-align: center;
  margin-left: 8px;
  /* Styles for the "isometric button" effect. */
  position: relative;
  top: -2px;
  _box-shadow: 0 2px 0 #c1c1c1;
}
#semantics .opName.selected {
  border-color: rgb(53, 151, 255);
  box-shadow: none;
  top: 0;
}
#semantics div.opName {
  cursor: default;
  -moz-user-select: none;
  -ms-user-select: none;
  -webkit-user-select: none;
}
